EventsWithKinds
== E:Type
==  (eq:EqDecider(E)
==  unused:Top
==  pred?:(E(?E))
==  info:(E((:Id  Id) + (:(:IdLnk  E)  Id)))
==  oaxioms:EOrderAxioms(E; pred?; info)
==  T:(IdIdType)
==  when:(x:Ide:ET(loc(e),x))
==  after:(x:Ide:ET(loc(e),x))
==  (saxiom:(e:E. ((first(e)))  (x:Id. when(x,e) = after(x,pred(e))))
==  Top)) 

latex

---

clarification:

EKind{i:l}
== E:Type{i}
==  (eq:EqDecider(E)
==  unused:Top
==  pred?:(E(E + Unit))
==  info:(E((:Id  Id) + (:(:IdLnk  E)  Id)))
==  oaxioms:EOrderAxioms{i}(E;
==  oaxioms:EOpred?;
==  oaxioms:EOinfo)
==  T:(IdIdType{i})
==  when:(x:Ide:ET(loc(info;e),x))
==  after:(x:Ide:ET(loc(info;e),x))
==  (saxiom:(e:E.
==  (saxiom:((first(pred?;e)))  (x:Id. when(x,e) = after(x,pred(pred?;e))  T(loc(info;e),x)))
==  Top)) 

latex

Definitions	EventsWithKinds, EqDecider(T), Unit, IdLnk, EOrderAxioms(E; pred?; info), P  Q, A, b, first(e), x:A. B(x), Id, loc(e), pred(e), Top
FDL editor aliases	EKind